Nuprl Lemma : mu-bound
11,40
postcript
pdf
b
:
,
f
:(int_seg(0;
b
)
). (
n
:int_seg(0;
b
). (
(
f
(
n
))))
(mu(
f
)
int_seg(0;
b
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
,
sq_type(
T
)
,
guard(
T
)
,
prop{i:l}
,
int_seg(
i
;
j
)
,
A
,
lelt(
i
;
j
;
k
)
,
P
Q
,
A
B
,
False
,
x
:
A
.
B
(
x
)
,
T
,
True
,
decidable(
P
)
,
P
Q
Lemmas
decidable
int
equal
,
le
wf
,
int
seg
wf
,
assert
wf
,
squash
wf
,
true
wf
,
bool
wf
origin
b:
, f:(int_seg(0; b)
). (
n:int_seg(0; b). (
(f(n)))) 
(mu(f) 
int_seg(0; b)) b:, f:(int_seg(0; b)). (n:int_seg(0; b). ((f(n)))) (mu(f) int_seg(0; b)) x:A. B(x) Q T
A
Q
Bx:A. B(x)
T
Q